T:Type, P:(T), as:(T List), d:Top.
(a:T. ((a  as) & (P(a))))  ((first a  as s.t. P(a) else d) = hd(filter(a.P(a);as))  T) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), P & Q, x(s), first x  as s.t. P(x) else d, hd(l), filter(P;l), reduce(f;k;as), Y, t  T, , if b then t else f fi , tt, ff, A c B, False, P  Q, {T}, , Unit, P  Q, A,
Lemmas	l member wf, assert wf, top wf, bool wf, nil member, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, cons member